Iof proof for Lemma bool cases sqequal:
1. b :
(b ~ tt) 
(b ~ ff)
by ((((((((D 1)
CollapseTHEN (D 1))
)
CollapseTHEN (Thin 1)))
CollapseTHEN (
CUnfolds ``btrue bfalse`` 0)))
CollapseTHEN (Fold `it` 0))
C1:
C1: (no hyps)
C1: ((inl ) ~ (inl )) ((inl ) ~ (inr ))
C2:
C2: (no hyps)
C2: ((inr ) ~ (inl )) ((inr ) ~ (inr ))
C.
T